$\forall$${\it es}$:ES, $p$:(E$\rightarrow$(E + Top)).
\\[0ex]causal{-}predecessor(${\it es}$;$p$) $\Rightarrow$ ($\forall$$e$, ${\it e'}$, $a$, $b$:E. $a$ c$\leq$ $e$ $\Rightarrow$ $e$ $p$$\leq$ ${\it e'}$ $\Rightarrow$ ${\it e'}$ $p$$<$ $b$ $\Rightarrow$ ($a$ $<$ $b$))